diff options
| -rw-r--r-- | kernel/instantiate.ml | 17 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 11 |
2 files changed, 22 insertions, 6 deletions
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index 27754ae841..c73fbd220d 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -24,7 +24,22 @@ let instantiate sign c args = else replace_vars inst c -let instantiate_evar = instantiate +(* Vérifier que les instances des let-in sont compatibles ?? *) +let instantiate_sign_including_let sign args = + let rec instrec = function + | ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args)) + | ([],[]) -> [] + | ([],_) | (_,[]) -> + anomaly "Signature and its instance do not match" + in + instrec (sign,args) + +let instantiate_evar sign c args = + let inst = instantiate_sign_including_let sign args in + if is_id_inst inst then + c + else + replace_vars inst c let instantiate_constr sign c args = if Options.immediate_discharge then diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index c155c45554..d7df2507cd 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -61,7 +61,7 @@ let dummy_sort = mkType dummy_univ let make_evar_instance env = fold_named_context - (fun env (id, b, _) l -> if b=None then mkVar id :: l else l) + (fun env (id, b, _) l -> (*if b=None then*) mkVar id :: l (*else l*)) env [] (* Declaring any type to be in the sort Type shouldn't be harmful since @@ -189,6 +189,7 @@ let real_clean isevars sp args rhs = else begin let (sigma,rc) = do_restrict_hyps !isevars ev args' in isevars := sigma; + rc end else @@ -204,18 +205,18 @@ let make_evar_instance_with_rel env = let n = rel_context_length (rel_context env) in let vars = fold_named_context - (fun env (id,b,_) l -> if b=None then mkVar id :: l else l) + (fun env (id,b,_) l -> (* if b=None then *) mkVar id :: l (*else l*)) env [] in snd (fold_rel_context - (fun env (_,b,_) (i,l) -> (i-1, if b=None then mkRel i :: l else l)) + (fun env (_,b,_) (i,l) -> (i-1, (*if b=None then *) mkRel i :: l (*else l*))) env (n,vars)) let make_subst env args = snd (fold_named_context (fun env (id,b,c) (args,l as g) -> match b, args with - | None, a::rest -> (rest, (id,a)::l) - | Some _, _ -> g + | (* None *) _ , a::rest -> (rest, (id,a)::l) +(* | Some _, _ -> g*) | _ -> anomaly "Instance does not match its signature") env (List.rev args,[])) |