i,canonical_context',(subst_in ty)
) metasenv'
in
- let bo' = subst_in bo in
+ let bo' = lazy (subst_in (Lazy.force bo)) in
(* Metavariables can appear also in the *statement* of the theorem
* since the parser does not reject as statements terms with
* metavariable therein *)
let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv =
let (uri,_,initial_subst,bo,ty, attrs) = proof in
let subst_in = CicMetaSubst.apply_subst subst in
- let bo' = subst_in bo in
+ let bo' = lazy (subst_in (Lazy.force bo)) in
(* Metavariables can appear also in the *statement* of the theorem
* since the parser does not reject as statements terms with
* metavariable therein *)
in
aux 1 context
+let find_hyp name =
+ let rec find_hyp n =
+ function
+ [] -> assert false
+ | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
+ Cic.Rel n, CicSubstitution.lift n ty
+ | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*)
+ | _::tl -> find_hyp (n+1) tl
+ in
+ find_hyp 1
+;;
+
+(* sort pattern hypotheses from the smallest to the highest Rel *)
+let sort_pattern_hyps context (t,hpatterns,cpattern) =
+ let hpatterns =
+ List.sort
+ (fun (id1,_) (id2,_) ->
+ let t1,_ = find_hyp id1 context in
+ let t2,_ = find_hyp id2 context in
+ match t1,t2 with
+ Cic.Rel n1, Cic.Rel n2 -> compare n1 n2
+ | _,_ -> assert false) hpatterns
+ in
+ t,hpatterns,cpattern
+;;
+
(* FG: **********************************************************************)
let get_name context index =