Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
| _ -> 0
Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
| _ -> 0
(* Assumption: The term "term" must be closed in the current context *)
let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic in
let (_,metasenv,_,_) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
(* Assumption: The term "term" must be closed in the current context *)
let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic in
let (_,metasenv,_,_) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
match term with
C.Var (uri,exp_named_subst) ->
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
match term with
C.Var (uri,exp_named_subst) ->
(CicMetaSubst.apply_subst subst), status
let apply_tac ~term status = snd (apply_tac_verbose ~term status)
(CicMetaSubst.apply_subst subst), status
let apply_tac ~term status = snd (apply_tac_verbose ~term status)
=
let module C = Cic in
let curi,metasenv,pbo,pty = proof in
=
let module C = Cic in
let curi,metasenv,pbo,pty = proof in
- let _,_ = (* TASSI: FIXME *)
+ if occur metano term then
+ raise
+ (ProofEngineTypes.Fail (lazy
+ "You can't letin a term containing the current goal"));
+ let _,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let newmeta = new_meta_of_proof ~proof in
let fresh_name =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let newmeta = new_meta_of_proof ~proof in
let fresh_name =