started work on reflecting inductive definitions.

Just created a new vernac command "Make Inductive".
As of now, it does nothing. Tested the dummy command in demo.v

src/.merlin

@@ -0,0 +1,20 @@
+FLG -rectypes
+
+B /home/abhishek/coq-8.5pl1/config
+B /home/abhishek/coq-8.5pl1/lib
+B /home/abhishek/coq-8.5pl1/intf
+B /home/abhishek/coq-8.5pl1/kernel
+B /home/abhishek/coq-8.5pl1/kernel/byterun
+B /home/abhishek/coq-8.5pl1/library
+B /home/abhishek/coq-8.5pl1/engine
+B /home/abhishek/coq-8.5pl1/pretyping
+B /home/abhishek/coq-8.5pl1/interp
+B /home/abhishek/coq-8.5pl1/proofs
+B /home/abhishek/coq-8.5pl1/tactics
+B /home/abhishek/coq-8.5pl1/printing
+B /home/abhishek/coq-8.5pl1/parsing
+B /home/abhishek/coq-8.5pl1/toplevel
+B /home/abhishek/coq-8.5pl1/tools
+B /home/abhishek/coq-8.5pl1/tools/coqdoc
+B /home/abhishek/coq-8.5pl1/dev
+

src/reify.ml4

@@ -12,6 +12,7 @@ let _ = Goptions.declare_bool_option {
   Goptions.optwrite = (fun a -> cast_prop:=a);
 }
 
+(*whether Set Template Cast Propositions is on, as needed for erasure in Certticoq*)
 let is_cast_prop () = !cast_prop                     
 
 let pp_constr fmt x = Pp.pp_with fmt (Printer.pr_constr x)
@@ -85,7 +86,8 @@ struct
   let pair a b f s =
     Term.mkApp (c_pair, [| a ; b ; f ; s |])
 
-  let nAnon = r_reify "nAnon"
+    (* reify the constructors in Template.Ast.v, which are the building blocks in reification *)
+  let nAnon = r_reify "nAnon" (* resolve_symbol pkg_reify *)
   let nNamed = r_reify "nNamed"
   let kVmCast = r_reify "VmCast"
   let kNative = r_reify "NativeCast"
@@ -766,6 +768,12 @@ VERNAC COMMAND EXTEND Unquote_vernac CLASSIFIED AS SIDEFF
 	  [] None result None (Lemmas.mk_hook (fun _ _ -> ())) ]
 END;;
 
+VERNAC COMMAND EXTEND Unquote_inductive CLASSIFIED AS SIDEFF
+    | [ "Make" "Inductive" ident(name) ":=" constr(def) ] ->
+      [ check_inside_section () ;
+	let (evm,env) = Lemmas.get_current_context () in () ]
+END;;
+
 VERNAC COMMAND EXTEND Make_tests CLASSIFIED AS QUERY
 (*
     | [ "Make" "Definitions" tactic(t) ] ->

test-suite/demo.v

@@ -30,6 +30,8 @@ Definition id_nat : nat -> nat := fun x => x.
 
 Quote Definition d'' := Eval compute in id_nat.
 
+Print d''.
+
 (** Fixpoints **)
 Fixpoint add (a b : nat) : nat :=
   match a with
@@ -44,17 +46,28 @@ Fixpoint add' (a b : nat) : nat :=
   end.
 
 Quote Definition add_syntax := Eval compute in add.
+Quote Definition natq := nat.
+Print natq.
+Quote Recursively Definition plus_syntax := plus.
+
+Print plus_syntax.
+
+
+Make Definition addss := ltac:(let t:= eval compute in d'' in exact t).
+
+Make Inductive addss := ltac:(let t:= eval compute in d'' in exact t).
 
 Quote Definition add'_syntax := Eval compute in add'.
 
 (** Reflecting definitions **)
 
 Make Definition zero_from_syntax := (Ast.tConstruct (Ast.mkInd "Coq.Init.Datatypes.nat" 0) 0).
 
+
+
 Make Definition two_from_syntax := (Ast.tApp (Ast.tConstruct (Ast.mkInd "Coq.Init.Datatypes.nat" 0) 1)
    (Ast.tApp (Ast.tConstruct (Ast.mkInd "Coq.Init.Datatypes.nat" 0) 1)
       (Ast.tConstruct (Ast.mkInd "Coq.Init.Datatypes.nat" 0) 0 :: nil) :: nil)).
 
-Quote Recursively Definition plus_syntax := plus.
 
 Quote Recursively Definition mult_syntax := mult.

test-suite/mutind.v

@@ -25,3 +25,5 @@ End with_T.
 Local Open Scope string_scope.
 Local Open Scope positive_scope.
 Quote Recursively Definition count_tree_syntax := count_tree.
+
+Print count_tree_syntax.