diff options
author | 1999-12-06 15:07:11 +0000 | |
---|---|---|
committer | 1999-12-06 15:07:11 +0000 | |
commit | 84c0f274e3baa424299c7b098ad7ced9ea4bab0e (patch) | |
tree | 77c010e4391739eca90d6c22b73c67df28326e6a /parsing | |
parent | 7d94e54e8dfa1d3d72d6c31f01dff49b701bcf99 (diff) |
declarations eliminations / debuggae inductifs (debut)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@212 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/pretty.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 0e062f6c9..f12f5edec 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -121,7 +121,7 @@ let implicit_args_msg sp mipv = [< (implicit_args_id mip.mind_typename (list_of_implicits imps)); prvecti (fun j idc -> - let imps = constructor_implicits ((sp,i),j) in + let imps = constructor_implicits ((sp,i),succ j) in (implicit_args_id idc (list_of_implicits imps))) mip.mind_consnames >]) @@ -245,7 +245,7 @@ let print_leaf_entry with_values sep (spopt,lobj) = hOV 0 [< 'sTR"Fw constant " ; 'sTR (print_basename (fwsp_of sp)) ; 'fNL>] - | (sp,"MUTUALINDUCTIVE") -> + | (sp,"INDUCTIVE") -> let mib = Global.lookup_mind sp in if kind_of_path sp = CCI then [< print_mutual sp mib; 'fNL >] @@ -369,7 +369,7 @@ let crible (fn:string -> unit assumptions -> constr -> unit) name = if (head_const typ.body) = const then fn (print_basename sp) hyps typ.body; crible_rec rest - | (sp,"MUTUALINDUCTIVE") -> + | (sp,"INDUCTIVE") -> let mib = Global.lookup_mind sp in (match const with | (DOPN(MutInd(sp',tyi),_)) -> @@ -490,11 +490,11 @@ let print_local_context () = [< print_last_const rest; 'sTR(print_basename sp) ;'sTR" = "; print_typed_recipe (val_0,typ) >] - | "MUTUALINDUCTIVE" -> + | "INDUCTIVE" -> let mib = Global.lookup_mind sp in [< print_last_const rest;print_mutual sp mib; 'fNL >] - | "VARIABLE" -> [< >] - | _ -> print_last_const rest) + | "VARIABLE" -> [< >] + | _ -> print_last_const rest) | (sp,Lib.ClosedSection _)::rest -> print_last_const rest | _ -> [< >] in @@ -583,7 +583,7 @@ let print_extraction () = (match cont with | Some(t,_) -> fprint_var (string_of_id name) t | _ -> [< >]) >] - | (sp,"MUTUALINDUCTIVE") -> + | (sp,"INDUCTIVE") -> [< print_rec rest; (try [< print_extracted_mutual sp ; 'fNL >] @@ -626,7 +626,7 @@ let print_extracted_context () = [< 'sTR (s ^" ==> "); fprint_recipe d; 'fNL >] with Not_found -> [< >]) >] - | "MUTUALINDUCTIVE" -> + | "INDUCTIVE" -> [< print_last_constants rest; try print_extracted_mutual sp with Not_found -> [<>] >] | "VARIABLE" -> |