diff options
| author |  gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-02 10:01:15 +0000 |
|---|---|---|
| committer | gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-02 10:01:15 +0000 |
| commit | bf578ad5e2f63b7a36aeaef5e0597101db1bd24a (patch) | |
| tree | c0bc4e5f9ae67b8a03b28134dab3dcfe31d184dd /contrib/recdef | |
| parent | 825a338a1ddf1685d55bb5193aa5da078a534e1c (diff) | |
Changement des named_context
Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/recdef')
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index aa7766785..4121580ff 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -132,7 +132,7 @@ let rec (find_call_occs: | Meta(_) -> error "find_call_occs : Meta" | Evar(_) -> error "find_call_occs : Evar" | Sort(_) -> error "find_call_occs : Sort" - | Cast(_,_) -> error "find_call_occs : cast" + | Cast(_,_,_) -> error "find_call_occs : cast" | Prod(_,_,_) -> error "find_call_occs : Prod" | Lambda(_,_,_) -> error "find_call_occs : Lambda" | LetIn(_,_,_,_) -> error "find_call_occs : let in" @@ -514,7 +514,7 @@ let com_terminate fonctional_ref input_type relation_ast wf_thm_ast let (proofs_constr:constr list) = List.map (fun x -> interp_constr evmap env x) proofs in (start_proof thm_name - (IsGlobal (Proof Lemma)) (Environ.named_context env) (hyp_terminates fonctional_ref) + (IsGlobal (Proof Lemma)) (Environ.named_context_val env) (hyp_terminates fonctional_ref) (fun _ _ -> ()); by (whole_start fonctional_ref input_type relation wf_thm proofs_constr); @@ -713,7 +713,7 @@ let (com_eqn : identifier -> let eq_constr = interp_constr evmap env eq in let f_constr = (constr_of_reference f_ref) in (start_proof eq_name (IsGlobal (Proof Lemma)) - (Environ.named_context env) eq_constr (fun _ _ -> ()); + (Environ.named_context_val env) eq_constr (fun _ _ -> ()); by (start_equation f_ref terminate_ref (fun x -> |