do_heavy_checks: bool ;
}
+let concat_nuris uris nuris =
+ match uris,nuris with
+ | `New uris, `New nuris -> `New (nuris@uris)
+ | _ -> assert false
+;;
(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
* names as long as they are available, then it fallbacks to name generation
* using FreshNamesGenerator module *)
| GrafiteAst.NConstructor (_loc,num,args) ->
NTactics.constructor_tac
?num ~args:(List.map (fun x -> text,prefix_len,x) args)
+ | GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t)
| GrafiteAst.NDot _ -> NTactics.dot_tac
| GrafiteAst.NElim (_loc, what, where) ->
NTactics.elim_tac
NTactics.generalize_tac ~where:(text,prefix_len,where)
| GrafiteAst.NId _ -> (fun x -> x)
| GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+ | GrafiteAst.NLApply (_loc, t) -> NTactics.lapply_tac (text,prefix_len,t)
| GrafiteAst.NLetIn (_loc,where,what,name) ->
NTactics.letin_tac ~where:(text,prefix_len,where)
~what:(text,prefix_len,what) name
eval_ncommand opts status
("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
in
- match uris,nuris with
- `New uris, `New nuris -> status,`New (nuris@uris)
- | _ -> assert false
+ status, concat_nuris uris nuris
with
NCicTypeChecker.TypeCheckerFailure msg
when Lazy.force msg =
(fun (name,is_coercion,arity) ->
if is_coercion then Some(name,leftno,arity) else None) fields
| _ -> [] in
- let status =
+ let status,uris =
List.fold_left
- (fun status (name,cpos,arity) ->
+ (fun (status,uris) (name,cpos,arity) ->
let metasenv,subst,status,t =
GrafiteDisambiguate.disambiguate_nterm None status [] [] []
("",0,CicNotationPt.Ident (name,None)) in
assert (metasenv = [] && subst = []);
- NCicCoercDeclaration.basic_eval_and_inject_ncoercion_from_t_cpos_arity
- status (name,t,cpos,arity)
- ) status coercions
+ let status, nuris =
+ NCicCoercDeclaration.
+ basic_eval_and_record_ncoercion_from_t_cpos_arity
+ status (name,t,cpos,arity)
+ in
+ let uris = concat_nuris nuris uris in
+ status, uris)
+ (status,uris) coercions
in
status,uris
with