diff options
author | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-09 16:35:28 +0000 |
---|---|---|
committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-09 16:35:28 +0000 |
commit | 40bc25786e53d7146d16218808e9b2de1cd59240 (patch) | |
tree | 96466d292c8a7f9ed34818cca03bdd18cac0b049 | |
parent | 36701f1900c8247d76436f2cf7ee09865b45ce3f (diff) |
bug de refine: uncaught exception Array.sub
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1443 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | tactics/refine.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/refine.ml b/tactics/refine.ml index 6c87782fc..dadda64de 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -168,12 +168,13 @@ let rec compute_metamap env c = match kind_of_term c with | IsMutCase (ci,p,c,v) -> (* bof... *) + let nbr = Array.length v in let v = Array.append [|p;c|] v in let a = Array.map (compute_metamap env) v in begin try let v',mm,sgp = replace_in_array env a in - let v'' = Array.sub v' 2 (Array.length v) in + let v'' = Array.sub v' 2 nbr in TH (mkMutCase (ci,v'.(0),v'.(1),v''),mm,sgp) with NoMeta -> TH (c,[],[]) |