diff options
| -rw-r--r-- | parsing/g_minicoq.ml4 | 11 | ||||
| -rw-r--r-- | toplevel/fhimsg.ml | 2 | ||||
| -rw-r--r-- | toplevel/minicoq.ml | 4 |
3 files changed, 11 insertions, 6 deletions
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4 index ae26e3f3c0..bf75cdd381 100644 --- a/parsing/g_minicoq.ml4 +++ b/parsing/g_minicoq.ml4 @@ -84,9 +84,14 @@ EXTEND end | "("; c = term; "::"; t = term; ")" -> DOP2 (Cast, c, t) - | "<"; p = term; ">"; IDENT "Case"; c = term; "of"; - bl = LIST0 term; "end" -> - DOPN (MutCase None, Array.of_list (p :: c :: bl)) + | "<"; p = term; ">"; + IDENT "Case"; c = term; ":"; "Ind"; id = IDENT; i = INT; + "of"; bl = LIST0 term; "end" -> + let ind = (path_of_string id,int_of_string i) in + let nc = List.length bl in + let dummy_pats = Array.create nc RegularPat in + let dummy_ci = [||],(ind,[||],nc,None,dummy_pats) in + DOPN (MutCase dummy_ci, Array.of_list (p :: c :: bl)) ] ]; command: [ [ "Definition"; id = IDENT; ":="; c = term; "." -> diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml index 419488a37b..45a922d7f1 100644 --- a/toplevel/fhimsg.ml +++ b/toplevel/fhimsg.ml @@ -53,7 +53,7 @@ module Make = functor (P : Printer) -> struct [< sign_env; db_env >] let pr_ne_ctx header k = function - | ENVIRON (([],[]),[]) -> [< >] + | ENVIRON (s1,s2) when s1=nil_sign & s2=nil_dbsign -> [< >] | env -> [< header; pr_env k env >] diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index a5e421feda..7af018585a 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -23,7 +23,7 @@ let lookup_var id = in look 1 -let args sign = Array.of_list (List.map (fun id -> VAR id) (fst sign)) +let args sign = Array.of_list (List.map (fun id -> VAR id) (ids_of_sign sign)) let rec globalize bv = function | VAR id -> lookup_var id bv @@ -51,7 +51,7 @@ let check c = let definition id ty c = let c = globalize [] c in let ty = option_app (globalize []) ty in - let ce = { const_entry_body = c; const_entry_type = ty } in + let ce = { const_entry_body = Cooked c; const_entry_type = ty } in let sp = make_path [] id CCI in env := add_constant sp ce !env; mSGNL (hOV 0 [< print_id id; 'sPC; 'sTR"is defined"; 'fNL >]) |